(0) Obligation:
Clauses:
div(X1, 0, X2, X3) :- ','(!, failure(a)).
div(0, X4, Z, R) :- ','(!, ','(eq(Z, 0), eq(R, 0))).
div(X, Y, s(Z), R) :- ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))).
div(X, X5, X6, X).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
eq(X, X).
Query: div(g,g,a,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
minusA(s(X1), s(X2), X3) :- minusA(X1, X2, X3).
divB(s(X1), s(X2), s(X3), X4) :- minusA(X1, X2, X5).
divB(s(X1), s(X2), s(X3), X4) :- ','(minuscA(X1, X2, X5), divB(X5, s(X2), X3, X4)).
Clauses:
minuscA(X1, 0, X1).
minuscA(s(X1), s(X2), X3) :- minuscA(X1, X2, X3).
divcB(0, X1, 0, 0).
divcB(s(X1), s(X2), s(X3), X4) :- ','(minuscA(X1, X2, X5), divcB(X5, s(X2), X3, X4)).
divcB(X1, X2, X3, X1).
divcB(X1, X2, X3, X1).
Afs:
divB(x1, x2, x3, x4) = divB(x1, x2)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
divB_in: (b,b,f,f)
minusA_in: (b,b,f)
minuscA_in: (b,b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → U2_GGAA(X1, X2, X3, X4, minusA_in_gga(X1, X2, X5))
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → MINUSA_IN_GGA(X1, X2, X5)
MINUSA_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, minusA_in_gga(X1, X2, X3))
MINUSA_IN_GGA(s(X1), s(X2), X3) → MINUSA_IN_GGA(X1, X2, X3)
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → U3_GGAA(X1, X2, X3, X4, minuscA_in_gga(X1, X2, X5))
U3_GGAA(X1, X2, X3, X4, minuscA_out_gga(X1, X2, X5)) → U4_GGAA(X1, X2, X3, X4, divB_in_ggaa(X5, s(X2), X3, X4))
U3_GGAA(X1, X2, X3, X4, minuscA_out_gga(X1, X2, X5)) → DIVB_IN_GGAA(X5, s(X2), X3, X4)
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0, X1) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2), X3) → U6_gga(X1, X2, X3, minuscA_in_gga(X1, X2, X3))
U6_gga(X1, X2, X3, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
divB_in_ggaa(
x1,
x2,
x3,
x4) =
divB_in_ggaa(
x1,
x2)
s(
x1) =
s(
x1)
minusA_in_gga(
x1,
x2,
x3) =
minusA_in_gga(
x1,
x2)
minuscA_in_gga(
x1,
x2,
x3) =
minuscA_in_gga(
x1,
x2)
0 =
0
minuscA_out_gga(
x1,
x2,
x3) =
minuscA_out_gga(
x1,
x2,
x3)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
DIVB_IN_GGAA(
x1,
x2,
x3,
x4) =
DIVB_IN_GGAA(
x1,
x2)
U2_GGAA(
x1,
x2,
x3,
x4,
x5) =
U2_GGAA(
x1,
x2,
x5)
MINUSA_IN_GGA(
x1,
x2,
x3) =
MINUSA_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGAA(
x1,
x2,
x3,
x4,
x5) =
U3_GGAA(
x1,
x2,
x5)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → U2_GGAA(X1, X2, X3, X4, minusA_in_gga(X1, X2, X5))
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → MINUSA_IN_GGA(X1, X2, X5)
MINUSA_IN_GGA(s(X1), s(X2), X3) → U1_GGA(X1, X2, X3, minusA_in_gga(X1, X2, X3))
MINUSA_IN_GGA(s(X1), s(X2), X3) → MINUSA_IN_GGA(X1, X2, X3)
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → U3_GGAA(X1, X2, X3, X4, minuscA_in_gga(X1, X2, X5))
U3_GGAA(X1, X2, X3, X4, minuscA_out_gga(X1, X2, X5)) → U4_GGAA(X1, X2, X3, X4, divB_in_ggaa(X5, s(X2), X3, X4))
U3_GGAA(X1, X2, X3, X4, minuscA_out_gga(X1, X2, X5)) → DIVB_IN_GGAA(X5, s(X2), X3, X4)
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0, X1) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2), X3) → U6_gga(X1, X2, X3, minuscA_in_gga(X1, X2, X3))
U6_gga(X1, X2, X3, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
divB_in_ggaa(
x1,
x2,
x3,
x4) =
divB_in_ggaa(
x1,
x2)
s(
x1) =
s(
x1)
minusA_in_gga(
x1,
x2,
x3) =
minusA_in_gga(
x1,
x2)
minuscA_in_gga(
x1,
x2,
x3) =
minuscA_in_gga(
x1,
x2)
0 =
0
minuscA_out_gga(
x1,
x2,
x3) =
minuscA_out_gga(
x1,
x2,
x3)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
DIVB_IN_GGAA(
x1,
x2,
x3,
x4) =
DIVB_IN_GGAA(
x1,
x2)
U2_GGAA(
x1,
x2,
x3,
x4,
x5) =
U2_GGAA(
x1,
x2,
x5)
MINUSA_IN_GGA(
x1,
x2,
x3) =
MINUSA_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U3_GGAA(
x1,
x2,
x3,
x4,
x5) =
U3_GGAA(
x1,
x2,
x5)
U4_GGAA(
x1,
x2,
x3,
x4,
x5) =
U4_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUSA_IN_GGA(s(X1), s(X2), X3) → MINUSA_IN_GGA(X1, X2, X3)
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0, X1) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2), X3) → U6_gga(X1, X2, X3, minuscA_in_gga(X1, X2, X3))
U6_gga(X1, X2, X3, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
minuscA_in_gga(
x1,
x2,
x3) =
minuscA_in_gga(
x1,
x2)
0 =
0
minuscA_out_gga(
x1,
x2,
x3) =
minuscA_out_gga(
x1,
x2,
x3)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
MINUSA_IN_GGA(
x1,
x2,
x3) =
MINUSA_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MINUSA_IN_GGA(s(X1), s(X2), X3) → MINUSA_IN_GGA(X1, X2, X3)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
MINUSA_IN_GGA(
x1,
x2,
x3) =
MINUSA_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUSA_IN_GGA(s(X1), s(X2)) → MINUSA_IN_GGA(X1, X2)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MINUSA_IN_GGA(s(X1), s(X2)) → MINUSA_IN_GGA(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DIVB_IN_GGAA(s(X1), s(X2), s(X3), X4) → U3_GGAA(X1, X2, X3, X4, minuscA_in_gga(X1, X2, X5))
U3_GGAA(X1, X2, X3, X4, minuscA_out_gga(X1, X2, X5)) → DIVB_IN_GGAA(X5, s(X2), X3, X4)
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0, X1) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2), X3) → U6_gga(X1, X2, X3, minuscA_in_gga(X1, X2, X3))
U6_gga(X1, X2, X3, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
minuscA_in_gga(
x1,
x2,
x3) =
minuscA_in_gga(
x1,
x2)
0 =
0
minuscA_out_gga(
x1,
x2,
x3) =
minuscA_out_gga(
x1,
x2,
x3)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
DIVB_IN_GGAA(
x1,
x2,
x3,
x4) =
DIVB_IN_GGAA(
x1,
x2)
U3_GGAA(
x1,
x2,
x3,
x4,
x5) =
U3_GGAA(
x1,
x2,
x5)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIVB_IN_GGAA(s(X1), s(X2)) → U3_GGAA(X1, X2, minuscA_in_gga(X1, X2))
U3_GGAA(X1, X2, minuscA_out_gga(X1, X2, X5)) → DIVB_IN_GGAA(X5, s(X2))
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2)) → U6_gga(X1, X2, minuscA_in_gga(X1, X2))
U6_gga(X1, X2, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
minuscA_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(17) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
DIVB_IN_GGAA(s(X1), s(X2)) → U3_GGAA(X1, X2, minuscA_in_gga(X1, X2))
U3_GGAA(X1, X2, minuscA_out_gga(X1, X2, X5)) → DIVB_IN_GGAA(X5, s(X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( U3_GGAA(x1, ..., x3) ) = 2x3 + 2
POL( minuscA_in_gga(x1, x2) ) = 2x1
POL( 0 ) = 0
POL( minuscA_out_gga(x1, ..., x3) ) = 2x2 + x3
POL( s(x1) ) = 2x1 + 1
POL( U6_gga(x1, ..., x3) ) = 2x3 + 2
POL( DIVB_IN_GGAA(x1, x2) ) = 2x1 + 1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
minuscA_in_gga(X1, 0) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2)) → U6_gga(X1, X2, minuscA_in_gga(X1, X2))
U6_gga(X1, X2, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
(18) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
minuscA_in_gga(X1, 0) → minuscA_out_gga(X1, 0, X1)
minuscA_in_gga(s(X1), s(X2)) → U6_gga(X1, X2, minuscA_in_gga(X1, X2))
U6_gga(X1, X2, minuscA_out_gga(X1, X2, X3)) → minuscA_out_gga(s(X1), s(X2), X3)
The set Q consists of the following terms:
minuscA_in_gga(x0, x1)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(19) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(20) YES